This section describes the format of the module interface descriptions contained in the next sections. There is one section per public module.
Each section begins with a module definition. A pseudo Oberon notation is used, which lists all exported items of a module, and only those. It begins with the keyword DEFINITION instead of MODULE, export marks are omitted (except read-only marks), and procedure bodies and the module body are left out as well. A type-bound procedure appears in the corresponding record declaration itself.
The hypothetical module "Dictionaries" serves as an example:
DEFINITION Dictionaries;
CONST maxElems = 32;
TYPE
Dictionary = POINTER TO DictionaryDesc;
DictionaryDesc = RECORD
elems-: INTEGER;
PROCEDURE (d: Dictionary) Put (string: ARRAY OF CHAR; VAR key: INTEGER);
PROCEDURE (d: Dictionary) Get (key: INTEGER; VAR string: ARRAY OF CHAR)
END;
VAR someDict: Dictionary;
PROCEDURE Init;
END Dictionaries.
In an extended record, the inherited procedures are not listed, only the new procedures. The only exception is an inherited function procedure which returns a pointer that is an extension of the one returned by the base procedure (covariant function result).
A module definition is followed by a brief description of the abstraction(s) provided by the module.
This module provides a concrete type Dictionary for the manipulation of string dictionaries.
Then the constants of the module are listed, without their values:
CONST maxElems
Maximum number of elements in a dictionary.
This is followed by the module's types. Record types are not described separately if a pointer type is available:
TYPE Dictionary
Interface
Manages a dictionary of strings, with an integer number as key.
Each type which serves as an interface type is marked as such, as above. An extension of a concrete type is never an interface type. Concrete types are not marked as such.
If the type is an extension of another type, this is marked, e.g. as
Interface, Extension
Base types are not marked as such.
Then the record fields are listed:
elems-: INTEGER 0 <= elems <= maxElems
The number of elements currently in the dictionary.
As in the above example, an invariant over the record field's value may optionally be given.
Then the procedures bound to this type are given:
PROCEDURE (d: Dictionary) Put (string: ARRAY OF CHAR; VAR key: INTEGER)
Interface
For each type-bound procedure, it is specified whether this procedure is interface, empty, default, or normal. An interface procedure may never be called. An empty procedure need never be called by an extending procedure (i.e. through a "super"-call of an "overriding" procedure). A default procedure may be replaced completely by an extending procedure. In this case, the extending procedure must implement the same behavior as the extended procedure. The Oberon/F documentation marks procedures as default procedures if they may be replaced by more efficient, but semantically equivalent implementations. Otherwise, concrete procedures implement some behavior and must always be called by extending procedures. An extension of an empty, a default, or a normal procedure is always marked the same way as its direct base procedure, or as a concrete procedure. Concrete procedures are not marked as such.
Every type which contains one or more interface procedures is an interface type.
For each type-bound procedure, it is specified whether this procedure is an extended procedure, i.e. whether a corresponding procedure already exists for its base type.
An explanation of the procedure's behavior follows:
Put a string into dictionary d, and receive key in return. If the string is already in the dictionary, the same key is returned as when it was inserted first. If the string is not in the dictionary, it is inserted and a value which has not been used before is returned.
After an explanation in plain English, some preconditions for this procedure may be specified. These preconditions are given in a semi-formal notation:
string # "" 20
This means that if the precondition is violated (i.e. if string = ""), the currently executing command is aborted with exception number 20. Instead of a number, the following exceptions may be specified as well:
invalid index
type guard check
A second precondition may thus be the following:
string in d OR d.elems < maxElems invalid index
After the preconditions, some postconditions may be specified as well:
string in d'
old key returned
~(string in d')
string in d
d.elems = d.elems' + 1
new key returned
This postcondition contains two cases, namely what happens if the string is already contained in d, and what happens if the string is not yet contained in d. The conditions are textually aligned to the left, while the respective conclusions are indented. Occasionally, conditions are nested by further indentations.
To refer to values before the operation, an expression is followed by an apostrophe if this is necessary for clarity (i.e. if the value may be changed at all). Thus the expression
d.elems = d.elems' + 1
means that the value of d.elems has been incremented by one.
Oberon is generally used as syntax for such expressions, although some liberties are taken, e.g. simple auxiliary procedures (which may not be described further) may be used, or expressions like "r.Base().Length()" are used (which are not legal in Oberon).
Function results are generically called "result".
The amount of formalism is kept small. It is attempted to limit formal specifications to few and simple conditions, or to the explanation of particularly subtle situations. It is not intended to specify complete formal semantics of the library, thus the formalism does not replace plain text explanations, examples, or graphical illustrations completely.
However, it is felt that checked preconditions in particular are often helpful even in this incomplete and semi-formal way, both for documentation and for debugging.
PROCEDURE (d: Dictionary) Get (key: INTEGER; VAR string: ARRAY OF CHAR)
Interface
Retrieve a string from the dictionary, by using key. If the value is not found, key is set to the empty string.
key in d
return corresponding string
~(key in d)
return ""
Procedures which are inherited through type extension are usually not listed here. Exceptions are procedures which have changed their semantics. The change in semantics is restricted to having weaker preconditions or stronger postconditions.
After all types, the global variables are listed:
VAR someDict: Dictionary someDict # NIL
This variable contains a dictionary.
The optional invariant is established by the module body.
Finally, the procedures exported by the module are listed:
PROCEDURE Init (d: Dictionary)
Initializes a dictionary. Any dictionary may be allocated once only.
d not yet initialized 20
In Oberon/F, all procedures whose names start with "Init" may be called only once per object.
(.txt)